Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
f
(x,
a
(
a
(
b
(
b
(y)))))
→
f
(
a
(
a
(
a
(
b
(
b
(
b
(x)))))),y)
2:
f
(
a
(x),y)
→
f
(x,
a
(y))
3:
f
(
b
(x),y)
→
f
(x,
b
(y))
There are 3 dependency pairs:
4:
F
(x,
a
(
a
(
b
(
b
(y)))))
→
F
(
a
(
a
(
a
(
b
(
b
(
b
(x)))))),y)
5:
F
(
a
(x),y)
→
F
(x,
a
(y))
6:
F
(
b
(x),y)
→
F
(x,
b
(y))
The approximated dependency graph contains one SCC: {4-6}.
Consider the SCC {4-6}. There are no usable rules.
The constraints could not be solved.
Tyrolean Termination Tool
(0.03 seconds) --- May 3, 2006